perm filename BIBLE[245,JMC] blob
sn#002383 filedate 1970-07-21 generic text, type T, neo UTF8
00100 BIBLIOGRAPHY
00200 AUTOMATIC DEDUCTION
00300
00400 A. GENERAL REVIEW
00500
00600 1963
00700
00800 Robinson, J.A., "Theorem Proving on the Computer", J. ACM,
00900 Vol. 10, pp. 163-174.
01000
01100 Wang, H., "Mechanical Mathematics and Inferential Analysis",
01200 in computer Programming and Formal Systems, Braffort
01300 and Hirschberg (Eds), N. Holland.
01400
01500 1967
01600
01700 Luckham, D., "The Resolution Principle in Theorem-Proving",
01800 Machine Intelligence 1, Collins and Michie (Eds)
01900 American Elsevier, Inc., New York,
02000
02002 Popplestone, R.J., "Beth-Tree Methods in Automatic Theorem
02004 Proving", Machine Intelligence I, Collins and
02006 Michie (eds.), Amer. Elsevier, New York.
02008
02100 Robinson, J.A., "A Review of Automatic Theorem Proving",
02200 Proc. of Symposia in Applied Mathematics, Vol. XIX
02300 American Mathematical Society.
02400
02500 Robinson, J.A., "Heuristic and Complete Processes in the
02600 Mechanization of Theorem-Proving", (Copy in
02700 CSD Library).
02800
02900
03000 B. FOUNDATIONS
03100
03102 1930
03104
03106 Herbrand, J., "Recherches sur la Theorie de la
03108 Demonstration", Traveaux de la Societe des
03110 Sciences et des Lettres de Varsovie, No. 33,
03112 128 pages.
03114
03200 1955
03300
03400 Quine, W.V., "A Proof Procedure for Quantification Theory",
03500 Journ. Symbolic Logic, V.20, p141.
03600
03700 1960
03800
03900 Davis, M., and Putnam, H., "A Computing Procedure for
04000 Quantification Theory", J. ACM, 7, July 1960,
04100 201.
04200
04300 Gilmore, P.C., "A Proof Method for Quantification Theory:
04400 Its Justification and Realization", IBM Journ. R+D
04500 V. 4, p 28.
04600
04700 Prawitz, D., Prawitz, H., and Voghera, N., "A Mechanical
04800 Proof Procedure and Its Realization in an Electronic
04900 Computer", JACM, V. 7, p 102.
05000
05100 Prawitz, D., "An Improved Proof Procedure", Theoria, V. 26,
05200 p. 102.
05300
05302 Wang, Hao, "Toward Mechanical Mathematics", IBM Journal of
05304 Res. Dev. 4, No. 1, pp. 2-22.
05306
05400 1963
05500
05600 Davis, M., "Eliminating the Irrelevant from Mechanical Proofs",
05700 Experimental Arithmetic, High Speed Computing and
05800 Mathematics, Proc. of Symposium in Appl. Math.,
05900 15, 15-30, Amer. Math. Soc., Prov., Rhode Island.
06000
06100 1965
06200
06300 Robinson, J.A., "A Machine-Oriented Logic Based on the
06400 Resolution Principle", Journal of the ACM, Vol. 12,
06500 No. 1, pp. 23-41, January 1965.
06600
06700 Robinson, J.A., "The Generalized Resolution Principle", Mach.
06800 Intelligence 3, D. Michie (Ed), Edinburgh Univ. Press,
06900 pp. 77-93.
07000
07100 C. REFINEMENTS OF THE BASIC PROOF PROCEDURES AND STRATEGIES
07200 TO IMPROVE EFFICIENCY
07300
07400 1964
07500
07600 Robinson, G. A., Wos, L.T., and Carson, D.F., "Some Theorem-
07700 Proving Strategies and Their Implementation", Argonne
07800 National Labs., Tech. Memorandum No. 72.
07900
08000 Wos, L., Carson, D., and Robinson, G., "The Unit Preference
08002 Strategy in Theorem Proving", AFIPS Conference
08004 Proceedings, vol. 26 (1964 Fall Joint Computer
08006 Conference), Spartan Books, Baltimore.
08008
08100 1965
08102
08200 Robinson, J., "Automatic Deduction with Hyper-Resolution",
08300 Intl Journal of Computer Mathematics, Vol. l,
08400 pp. 227-234.
08500
08600 Wos, L., et. al., "Efficiency and Completeness of the
08700 Set of Support Strategy in Theorem Proving ", J. ACM,
08800 Vol. 12, 4, pp 536-54l, October.
08900
09000 1966
09100
09200 Meltzer, B., "Theorem-Proving for Computers: Some Results on
09300 Resolution and Renaming", The Computer Journal,
09400 Vol. 8, pp. 341-343.
09500
09600 1967
09700
09800 Slagle, J.R., "Automatic Theorem-Proving with Renamable
09900 and Semantic Resolution", J. ACM, 14, pp. 687-697,
10000 October.
10100
10200 1968
10300
10400 Andrews, P.B., "Resolution With Merging", JACM, 15,
10500 No. 3, pp. 367-381, July.
10600
10700 Loveland, D., "Mechanical Theorem-Proving by Model Elimination",
10800 JACM, 15, No. 21, pp. 236-251, April.
10900
11000 Luckham, D., "Some Tree-Paring Strategies for Theorem-
11100 Proving", Machine Intelligence 3, D. Michie (Ed),
11200 Edinburgh University Press, pp. 95-112.
11300
11400 1969
11500
11600 Kowalski, R. and P. Hayes, "Semantic Trees in Automatic
11700 Theorem-Provings", Machine Intelligence 4, D. Michie
11800 (Ed), (to appear - 1969).
11900
11902 Loveland, D.W., "A Simplified Format for the Model Elimination
11904 Theorem Proving Procedure", J. ACM 16, No. 3, pp. 349-363.
11906
12000 1970
12100
12200 Kieburtz, R., Luckham, D., "Compatibility of Refinements of
12300 the Resolution Principle", Submitted to the JACM
12400 (March 1970).
12500
12600 Kowalski, R. "Studies in the Completeness and Efficiency of
12700 Theorem-Proving by Resolution", Dissertation, University
12800 of Edinburgh, 1970.
12900
13000 Loveland, D., "A Linear Format for Resolution", Proceedings
13100 IRIA Symposium on Automatic Demonstration, Versailles,
13200 France, December 16-21, 1968, Springer-Verlag,
13300 1970, pp. 147-162.
13400
13500 Luckham, D., "Refinement Theorems in Resolution Theory",
13600 Proceedings IRIA Symposium on Automatic Demonstration,
13700 Versailles, France, December 16-21, 1968, Springer-
13800 Verlag, 1970, pp. 163-190.
13900
13902 Yates, R., Raphael, B., Hart, T., "Resolution Graphs", Stanford
13904 Research Institute Artificial Intelligence Group
13906 Report No. 24. (To appear in the Artificial Intelligence
13908 Journal).
13910
14000
14100 D. REPORTS OF PROGRAMS AND RESULTS
14200
14202 1962
14204
14206 Davis, M., Logemann, G., and Loveland, D., "A Machine Program
14208 for Theorem Proving", C. ACM 5, No. 7, pp. 394-397.
14210
14300 1966
14400
14500 Norton, L., "ADEPT - a Heuristic Program for Proving Theorems
14600 of Group Theory", Ph.D. Thesis, MIT Project MAC
14700 TR-33.
14800
14900 1969
15000
15100 Guard, J.R., Oglesby, F.C., Bennett, J.H., Settle, L.G.,
15200 "Semi-Automated Mathematics", JACM, 16, No. 1, pp 49-62,
15300 January.
15400
15500 1970
15600
15700 Allen, J., Luckham, D., "An Interactive Theorem-Proving
15800 Program", MACHINE INTELLIGENCE 5, B. Meltzer and D.
15900 Michie (Eds), Edinburgh University Press, March.
16000
16100
16200 E. COMPUTATIONAL INFERENCE RULES FOR EQUALITY
16300
16400 1969
16500
16600 Robinson, G., and Wos, L., "Paramodulation and Theorem-Proving
16700 In First-Order Theories with Equality", MACHINE
16800 INTELLIGENCE IV, D. Michie (Ed).
16900
17000 Wos, L., et. al., "The Concept of Demodulation in Theorem-
17100 Proving", JACM, 14, No. 4, pp 698-704.
17200
17300 1970
17400
17500 Kowalski, R. "The case for Using Equality Axioms in Automatic
17600 Demonstration", Proc. IRIA Symposiums on Automatic
17700 Demonstration, Versailles, France, December 1968.
17800 Springer-Verlag, 1970, pp. 112-127.
17900
18000 Wos, L., and Robinson, G., "Paramodulation and Set of Support",
18050 Proc. IRIA Symposium on Automatic Demonstration,
18075 Versailles, France, December 1968. Springer-Verlag,
18087 1970, pp. 276-310.
18093
18100 F. APPLICATIONS
18200
18300 1965
18400
18500 Wang, H., "Formalization and Automatic Theorem-Proving",
18600 Proc. IFIP Congress 65, Vol. l, pp. 51-58, Spartan
18700 Books, Washington D.C..
18800
18900 1967
19000
19100 Bennett, J.H., et. al., "CRT-Aided Semi-Automated Mathematics,
19200 Report AFCRL-67-0167, Applied Logic Corporation,
19300 Princeton, New Jersey.
19400
19500 Green C., and Raphael, B., "Research on Intelligence Question-
19600 Answering Systems", SRI Report prepared under
19700 Contract AF19(628)-5919, May.
19800
19900 1968
20000
20100 Green, C., and Raphael, "The Use of Theorem-Proving Techniques
20200 in Question Answering Systems", Proc. ACM Conf.,
20300 Las Vegas, Nevada, August.
20400
20500 McCarthy, J., and P. Hayes, "Some Philosophical Problems
20600 from the Standpoint of Artificial Intelligence",
20700 Stanford University A.I. Project Memo No. AI-73,
20800 November.
20900
21000 1969
21100
21200 Green, C., "Theorem-Proving by Resolution as a Basis for
21300 Question-Answering Systems", MACHINE INTELLIGENCE 4,
21400 D. Michie, (Ed).
21500
21600 Nilsson, N.J., "A Mobile Automaton - An Application of
21700 Artificial Intelligence Techniques", Proc. Int'l Joint
21800 Conference on Artificial Intelligence, May.
21900
22000
22002 1970
22004
22006 Luckham, D., and Nilsson, N., "Extracting Information from
22008 Resolution Proof Trees", Stanford University A.I. Project
22010 Memo (forthcoming), submitted to the A.I. Journal
22012 (June 1970).
22014
22016 Robinson, G., and Wos, L., "Axiom Systems in Automatic Theorem-
22018 Proving", Proc. IRIA Symposium on Automatic Demonstration,
22020 Versailles, France, December 1968, Springer-Verlag,
22022 1970, pp. 215-236.
22024
22026
22100 G. MISCELLANEOUS
22200
22202 1963
22204
22206 Friedman, J., "A Semi-Decision Procedure for the Functional
22208 Calculus", J. ACM 10, vol. 1, pp. 1-24.
22210
22300 1968
22400
22500 Kallick, B., "A Decision Procedure Based on the Resolution
22600 Method", Proc. IFIP Congress 68, Edinburgh, Scotland,.
22700
22800 Robinson, J.A., "New Directions in Mechanical Theorem-Proving",
22900 Proc. IFIP Congress, 1968, Edinburgh.
23000
23100